algorithm An algorithm for proving a goal by recursively

braking it down into sub-goals and trying to prove these until

facts are reached. Facts are goals with no sub-goals which

are therefore always true. Backward training is the program

execution mechanism used by most logic programming language

like Prolog.